package edu.uic.cs.cs582.process.impl;

import java.util.Set;

import org.sat4j.specs.IConstr;
import org.sat4j.specs.Lbool;
import org.sat4j.specs.SearchListener;

import edu.uic.cs.cs582.data.Component;
import edu.uic.cs.cs582.process.impl.SatIndexParser.Index;
import edu.uic.cs.cs582.process.impl.SatIndexParser.SynsetIndex;
import edu.uic.cs.cs582.process.impl.SatIndexParser.WordIndex;

/**
 * {@link #conflictFound(IConstr, int, int)} interface is invoked 
 * whenever there's a conflict in the TRYING stage to find a solution
 * 
 * It is not the final real conflict!
 */
@Deprecated
class ConflictDetectingListener implements SearchListener
{
	private static final long serialVersionUID = 8293529582321500957L;

	private Set<Integer> conflictSynsetIndexes = null;
	private Set<Integer> conflictWordIndexes = null;

	private Component component = null;

	public ConflictDetectingListener(Set<Integer> conflictSynsetIndexes,
			Set<Integer> conflictWordIndexes, Component component)
	{
		this.conflictSynsetIndexes = conflictSynsetIndexes;
		this.conflictWordIndexes = conflictWordIndexes;
		this.component = component;
	}

	@Override
	public void conflictFound(IConstr confl, int dlevel, int trailLevel)
	{
		throw new UnsupportedOperationException();

		// Assert.isTrue(confl instanceof BinaryClause);

		//		System.out.print("==== " + dlevel + " " + trailLevel + " [");
		//		for (int index = 0; index < confl.size(); index++)
		//		{
		//			String conflict = Lits.toString(confl.get(index));
		//			collectConflictSynsetsOrWords(conflict);
		//		}
		//		System.out.println("]");
	}

	private void collectConflictSynsetsOrWords(String variable)
	{
		int indexReturnedBySat = Integer.parseInt(variable);
		System.out.print(indexReturnedBySat + " ");
		Index index = SatIndexParser.parseIndex(indexReturnedBySat, component);
		if (index instanceof SynsetIndex)
		{
			conflictSynsetIndexes.add(((SynsetIndex) index).getSynsetIndex());
			//			System.out.println("*************** processed synset: "
			//					+ component.getSynsetByIndex(((SynsetIndex) index)
			//							.getSynsetIndex()));
		}
		else if (index instanceof WordIndex)
		{
			conflictWordIndexes.add(((WordIndex) index)
					.getWordIndexInOneComponent());
			//			System.out.println("*************** processed word: "
			//					+ component.getWordByIndex(((WordIndex) index)
			//							.getWordIndexInOneComponent()));
		}
	}

	@Override
	public void conflictFound(int p)
	{
		// It seems never be called
		throw new UnsupportedOperationException();
	}

	@Override
	public void assuming(int p)
	{
	}

	@Override
	public void propagating(int p, IConstr reason)
	{
	}

	@Override
	public void backtracking(int p)
	{
	}

	@Override
	public void adding(int p)
	{
	}

	@Override
	public void learn(IConstr c)
	{
	}

	@Override
	public void delete(int[] clause)
	{
	}

	@Override
	public void solutionFound()
	{
	}

	@Override
	public void beginLoop()
	{
	}

	@Override
	public void start()
	{
	}

	@Override
	public void end(Lbool result)
	{
	}

	@Override
	public void restarting()
	{
	}

	@Override
	public void backjump(int backjumpLevel)
	{
	}

}
